Nuprl Lemma : imax_lb
12,41
postcript
pdf
a
,
b
,
c
:
. (imax(
a
;
b
)
c
)
{(
a
c
) & (
b
c
)}
latex
ProofTree
Definitions
True
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
bnot
wf
,
lt
int
wf
,
le
wf
,
assert
wf
,
bool
wf
,
le
int
wf
origin
a, b, c:
. (imax(a;b) 
c) 
{(a c) & (b c)}
a, b, c:. (imax(a;b) c) {(a c) & (b c)}
Q Q Q
Tx:A. B(x)